Inference at * 
Iof proof for Lemma do-apply-p-restrict:


  A, B:Type, f:(A(B + Top)), P:(A), p:(x:A. Dec(P(x))), x:A.
  (can-apply(p-restrict(f;p);x))  (do-apply(p-restrict(f;p);x) = do-apply(f;x)) 

latex

 by ((((Unfold `p-restrict` 0) 
CollapseTHEN (((Auto) 
CollapseTHEN (((((RWO "do-apply-compose" 0)

THEN (Auto))) 
CollapseTHEN (((((RWO "can-apply-compose-iff" (-1)) 
THEN (Auto))) 

THCollapseTHEN (((RWO "do-apply-p-filter" 0) 
THEN (Auto))))))))))) 
CollapseTHEN (((
CoAll (RWO "do-apply-p-filter")) 
CollapseTHEN (Auto)))) 

latex

Co.

Definitions	p-restrict(f;p), Dec(P), s = t, P  Q, P & Q, x:A  B(x), P  Q, b, , , can-apply(f;x), do-apply(f;x), p-filter(f), Type, left + right, Top, T, True, t  T, x(s), f(a), x. t(x), x:A. B(x), P  Q, x:AB(x)
Lemmas	do-apply-compose, can-apply-compose-iff, do-apply wf, assert wf, can-apply wf, do-apply-p-filter